\begin{nusmvCommand}{check\_invar\_bmc}{\label{checkInvarBmcCommand}
Generates and solves the given invariant, or all invariants if no
 formula is given}
 
\cmdLine{check\_invar\_bmc [-h | -n idx | -p "formula" [IN context]] [-a alg] 
[-o filename]}

In Bounded Model Checking, invariants are proved using induction. For
this, satisfiability problems for the base and induction step are
generated and a SAT solver is invoked on each of them. At the moment,
two algorithms can be used to prove invariants. In one algorithm,
which we call ``classic'', the base and induction steps are built on
one state and one transition, respectively.  Another algorithm, which
we call ``een-sorensson'' \cite{een04temporal}, can build the base and
induction steps on many states and transitions. As a result, the
second algorithm is more powerful.

Also, notice that during checking of invariants all the fairness
conditions associated with the model are ignored.

\begin{cmdOpt}

\opt{-n \parameter{\natnum{\it index}}} { {\it index} is the numeric
index of a valid INVAR specification formula actually located in the
property database.  The validity of {\it index} value is checked out
by the system.}
       
\opt{-p \parameter{"\anyexpr [IN context]"}}{ Checks the \anyexpr specified
on the command-line. \code{context} is the module instance name which
the variables in \anyexpr must be evaluated in.}
            
\opt{-k \parameter{\natnum{\it max\_length}}}{\natnum{\it max\_length}
is the maximum problem bound that can be reached. Only natural numbers
are valid values for this option. Use this option only if the
``een-sorensson'' algorithm is selected. If no value is given the
environment variable \envvar{\it bmc\_length} is considered instead.}

\opt{-a \parameter{\natnum{\it alg}}}{\natnum{\it alg} specifies the
algorithm.  The value can be \code{classic} or
\code{een-sorensson}. If no value is given the environment variable
\envvar{\it bmc\_invar\_alg} is considered instead.}

\opt{-o \parameter{\filename{\it filename}}}{ {\it filename} is the name of the dumped
dimacs file.  It may contain special symbols which will be
macro-expanded to form the real file name. Possible symbols are: }
       \tabItem{ @\textbf{F}: model name with path part }
       \tabItem{ @\textbf{f}: model name without path part} 
       \tabItem{ @\textbf{n}: index of the currently processed formula in the properties 
       database }
       \tabItem{ @@: the `@' character}

\end{cmdOpt}

\end{nusmvCommand}
